$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$:$A$, $v$, $z$, $f$:Top. $x$ : $v$ $\oplus$ $f$($x$)?$z$ $\sim$ $v$